functor PtrProof (S : PTRPROOF_STRUCTS) : PTRPROOF =
struct
  open S


  structure E = ErrorMsg
  structure S = Irvc2vc
  structure I = S.Ir
  structure T = I.Types
  structure V = S.Vc
  structure C = Control

  local open Irvc2vc.Ir
  in structure Id = Id
     structure Intl = Intl
  end

  local open I
  in structure B = Binop
  end

  exception shouldInU

  val error = ErrorMsg.error

  structure NDSet = BinarySetFn (struct
                                   type ord_key = V.lval
                                   val compare = V.compare
                                 end)

  fun ndCompare2 (set1, set2) =
      let val size1 = NDSet.numItems set1
          val size2 = NDSet.numItems set2
      in  if size1 <> size2
          then LESS
          else let val l1 = NDSet.listItems set1
                   val l2 = NDSet.listItems set2
                   fun inList (aptr, list) =
                       case list
                        of [] => 0
                         | a::l =>
                           (case V.compare (a, aptr)
                             of EQUAL => 1
                              | _ => inList (aptr, l))
                   val fl = List.map (fn aptr => inList (aptr, l2)) l1
                   val n = List.foldl (op +) 0 fl
               in  if n = size1
                   then EQUAL
                   else LESS
               end
      end

  structure PiSet = BinarySetFn (struct
                                   type ord_key = NDSet.set
                                   val compare = ndCompare2
                                 end)

  datatype pointerSort
    = Pi | N | D | U

  type settype = PiSet.set * NDSet.set * NDSet.set * PiSet.set

  val emptyPi = PiSet.empty
  val emptyN = NDSet.empty
  val emptyD = NDSet.empty
  val emptyU = PiSet.empty

  fun lval2vc lvalList = List.map (S.tr_l) lvalList

  fun toSet lvalList =
      let val new = lval2vc lvalList
      in  NDSet.addList(NDSet.empty, new)
      end

  fun toSetSet lvalss = PiSet.addList(PiSet.empty, List.map toSet lvalss)

  val iniPi = ref emptyPi
  val resetIniPi = fn () => (iniPi := emptyPi)

  fun debugPrint s = if (!C.doShowSrcPtrProof) then print s else ()

  fun printSet set =
      if (!C.doShowSrcPtrProof)
      then (print "{"; List.app print (List.map (V.lval2str) (NDSet.listItems set)); print "}")
      else ()

  fun printN set =
      if (!C.doShowSrcPtrProof)
      then (print "N = {"; List.app print (List.map (V.lval2str) (NDSet.listItems set)); print "}")
      else ()

  fun printD set =
      if (!C.doShowSrcPtrProof)
      then (print "D = {"; List.app print (List.map (V.lval2str) (NDSet.listItems set)); print "}")
      else ()

  fun printPi setSet =
      if (!C.doShowSrcPtrProof)
      then (print "\\Pi = {";PiSet.app printSet setSet; print "}\n")
      else ()

  fun printU setSet =
      if (!C.doShowSrcPtrProof)
      then (print "U = {";PiSet.app printSet setSet; print "}\n")
      else ()

  fun printPiND (pi, n, d, u) =
      (printPi pi
      ; printN n
      ; debugPrint "\n"
      ; printD d
      ; debugPrint "\n"
      ; printU u)

  val sayPointer = V.lval2str

  fun eqPi (pi1, pi2) = PiSet.equal (pi1, pi2)

  fun eqN (set1, set2) =
      let val size1 = NDSet.numItems set1
          val size2 = NDSet.numItems set2
      in  if size1 <> size2
          then false
          else let val l1 = NDSet.listItems set1
                   val l2 = NDSet.listItems set2
                   fun inList (aptr, list) =
                       case list
                        of [] => 0
                         | a::l =>
                           (case V.compare (a, aptr)
                             of EQUAL => 1
                              | _ => inList (aptr, l))
                   val fl = List.map (fn aptr => inList (aptr, l2)) l1
                   val n = List.foldl (op +) 0 fl
               in  if n = size1
                   then true
                   else false
               end
      end

  fun eqD (d1, d2) = eqN (d1, d2)

  fun isEmptyPi pi = PiSet.isEmpty pi
  fun isEmptyN n = NDSet.isEmpty n
  fun isEmptyD d = NDSet.isEmpty d

  fun isSingletonSet n = (NDSet.numItems n = 1)

  fun getPtrSet (ptr, pi) =
      let fun get l =
              case l
               of [] => (emptyN)
                | x :: xs =>
                  if isPtrInN (ptr, x)
                  then x
                  else (get xs)
      in  get (PiSet.listItems pi)
      end

  and isPtrInPi (ptr, pi) =
      let fun check l =
              case l
               of [] => false
                | x :: xs =>
                  if isPtrInN (ptr, x)
                  then true
                  else (check xs)
      in  check (PiSet.listItems pi)
      end

  and isPtrInU (ptr, u) = isPtrInPi (ptr, u)

  and isPtrInSingletonPi (ptr, pi) =
      let fun check l =
              case l
               of [] => false
                | x :: xs =>
                  if isPtrInN (ptr, x)
                  then if NDSet.numItems x = 1
                       then true
                       else false
                  else (check xs)
      in  check (PiSet.listItems pi)
      end

  and isPtrInN (ptr, n) =
      let fun check l =
              case l
               of [] => false
                | x :: xs =>
                  if x=ptr
                  then true
                  else (check xs)
      in  check (NDSet.listItems n)
      end

  and isPtrInD (ptr, d) =
      let fun check l =
              case l
               of [] => false
                | x :: xs =>
                  if x=ptr
                  then true
                  else (check xs)
      in  check (NDSet.listItems d)
      end

  and getPtrSort (ptr, pi, n, d, u) =
      if isPtrInPi (ptr, pi)
      then Pi
      else if isPtrInN (ptr, n)
           then N
           else if isPtrInD (ptr, d)
                then D
                else if isPtrInU (ptr, u)
                     then U
                     else (debugPrint (String.concat ["can not find lval : ", sayPointer ptr, "\n\n"])
                         ; U)

  and isSingletonN n =
      if NDSet.numItems n = 1
      then true
      else false

  and addPi (ptr, pi) =
      let val setOfPtr = NDSet.singleton ptr
      in  PiSet.add (pi, setOfPtr)
      end

  and addU (ptr, u) = addPi (ptr, u)

  and addSetPi (set, pi) = PiSet.add (pi, set)
  and addSetU (set, u) = PiSet.add (u, set)

  and addPtrPi (ptr, aim, pi) =
      let fun check l =
              case l
               of [] => raise Fail "bug?\n"
                | x :: xs =>
                  if isPtrInN (aim, x)
                  then (NDSet.add (x, ptr)) :: xs
                  else (x :: (check xs))
      in  PiSet.addList (emptyPi, check (PiSet.listItems pi))
      end
  and addPtrU (ptr, aim, u) = addPtrPi (ptr, aim, u)
  and addN (ptr, n) = NDSet.add (n, ptr)
  and addSetN (set1, set2) = NDSet.union (set1, set2)
  and addD (ptr, d) = NDSet.add (d, ptr)
  and deleteSetPi (set, pi) =
      if isEmptyN set
      then pi
      else if PiSet.member(pi, set)
           then PiSet.delete(pi, set)
           else (debugPrint "no such element in function delete \\Pi\n"; emptyPi)
  and deleteSetU (set, u) = deleteSetPi (set, u)

  and deletePtrPi (ptr, pi) =
      let val _ = debugPrint "see me\n"
          val _ = printPi pi
          val filterPi = getPtrSet (ptr, pi)
          val _ = printN filterPi
          val npi = if isPtrInSingletonPi (ptr, pi)
                    then (debugPrint "goes true branch\n"; deleteSetPi (filterPi, pi))
                    else if NDSet.isEmpty filterPi
                         then (debugPrint "bug in deletePtrPi?\n\n\n"; pi)
                         else let val tpi = deleteSetPi (filterPi, pi)
                                  val _ = printPi tpi
                                  val subset = filterPi
                                  val _ = debugPrint "to hererererererer\n"
                                  val _ = printN subset
                                  val tset = NDSet.delete (subset, ptr)
                                  val _ = printN tset
                                  val fpi = PiSet.add (tpi, tset)
                              in  fpi
                              end
      in  debugPrint "see me again\n"
         ; printPi npi
         ; npi
      end
  and deletePtrU (ptr, u) = deletePtrPi (ptr, u)
  and deletePtrN (ptr, n) = NDSet.delete(n, ptr)
  and deletePtrD (ptr, d) = NDSet.delete(d, ptr)

  fun deletePtrSetPi (ptr, pi) =
      let val set = getPtrSet (ptr, pi)
      in  PiSet.delete (pi, set)
      end

  fun deletePtrSetU (ptr, u) = deletePtrSetPi (ptr, u)

  fun isAllLongId n =
      let fun ck lvals =
              case lvals
               of [] => true
                | x :: xs =>
                  if V.isStruct2 x
                  then ck xs
                  else false
      in  ck (NDSet.listItems n)
      end

  fun implyPi (pi1, pi2) =
      let fun del setList =
              case setList
               of [] => []
                | x :: xs =>
                  if isAllLongId x
                  then (debugPrint "delete one\n\n\n\n\n\n\n";del xs)
                  else x :: (del xs)
          val pix = PiSet.addList (emptyPi, del (PiSet.listItems pi2))
      in  debugPrint "now compare:\n"
        ; printPi (pi1)
        ; printPi (pix)
        ; eqPi (pi1, pix)
      end

  fun postImplyPi2 (pi1, pi2) =
      let val _ = debugPrint "now compare:\n"
          val _ = printPi pi1
          val _ = printPi pi2
      in  PiSet.isSubset (pi2, pi1)
      end

  fun postImplyPi (pi1, pi2) =
      let val _ = debugPrint "now compare:\n"
          val _ = printPi pi1
          val _ = printPi pi2
      in  eqPi (pi2, pi1)
      end

  fun postImplyN (n1, n2) =
      let val _ = debugPrint "now compare:\n"
          val _ = printN n1
          val _ = printN n2
      in  eqN (n2, n1)
      end

  fun testLongId () =
      let val (lval1, lval2) = V.twoLongIds ()
          val (set1, set2) = (NDSet.addList (emptyN, [lval1]), NDSet.addList (emptyN, [lval1]))
      in  if eqN (set1, set2)
          then debugPrint "two long ids are equal\n\n\n\n\n\n"
          else debugPrint "not equal\n\n\n\n\n\n"
      end

  fun existsLongLvalN n = List.exists (fn lval => V.isStruct2 lval)
                                     (NDSet.listItems n)

  fun existsLongLvalPi pi = List.exists (fn n => existsLongLvalN n)
                                        (PiSet.listItems pi)

  fun findAlias (lval, set) =
      let fun find l =
          case l
           of [] => raise Fail "singleton set?\n\n\n"
            | x :: xs => x
      in  find (NDSet.listItems set)
      end

  fun adjustSet (lval, sub, set) =
      let fun subst l =
              case l
               of [] => []
                | x :: xs =>
                  (debugPrint "to ajust set\n\n\n\n"
                 ; (V.subst (lval, x, sub)) :: (subst xs))
          val lvals = subst (NDSet.listItems set)
          val newSet = NDSet.addList (emptyN, lvals)

          val _ = debugPrint "the set before ajust is :\n"
          val _ = printSet set
          val _ = debugPrint "\n"
          val _ = debugPrint "the set after ajust is :\n"
          val _ = printSet set
          val _ = debugPrint "\n"
      in  newSet
      end

  fun adjustSets (lval, sub, sets) =
      let fun subst l =
              case l
               of [] => []
                | x :: xs => adjustSet (lval, sub, x) :: subst xs
      in  PiSet.addList (emptyPi, subst (PiSet.listItems sets))
      end


  fun adjustPiNDU (lval, pi, n, d, u) =
      let val set = getPtrSet (lval, pi)
          val rem = deleteSetPi (set, pi)
          val alias = findAlias (lval, deletePtrN (lval, set))
          val newPi = adjustSets (lval, alias, rem)
          val n1 = adjustSet (lval, alias, n)
          val d1 = adjustSet (lval, alias, d)
          val u1 = adjustSets (lval, alias, u)
          val pi1 = addSetPi (set, newPi)
          val _ = debugPrint (String.concat ["try to ajust : ", sayPointer lval, "\n"])
          val _ = debugPrint (String.concat ["ajust it to : ", sayPointer alias, "\n"])
          val _ = debugPrint "the \\Pi set before ajust is :\n"
          val _ = printPiND (pi, n, d, u)
          val _ = debugPrint "the \\Pi set after ajust is :\n"
          val _ = printPiND (pi1, n, d, u)
      in  (pi1, n1, d1, u1)
      end

  fun adjustDelSet (lval, set) =
      let fun subst l =
              case l
               of [] => []
                | x :: xs =>
                  let val newLval = V.substDel (lval, x)
                      val _ = debugPrint "to ajust set\n\n\n\n"
                  in  case newLval
                       of V.Var "@@@Del" => subst xs
                        | _ => x :: (subst xs)
                  end
          val lvals = subst (NDSet.listItems set)
          val newSet = NDSet.addList (emptyN, lvals)

          val _ = debugPrint "the set before ajust is :\n"
          val _ = printSet set
          val _ = debugPrint "\n"
          val _ = debugPrint "the set after ajust is :\n"
          val _ = printSet set
          val _ = debugPrint "\n"
      in  newSet
      end

  fun adjustDelSets (lval, sets) =
      let fun subst l =
              case l
               of [] => []
                | x :: xs => adjustDelSet (lval, x) :: subst xs
      in  PiSet.addList (emptyPi, subst (PiSet.listItems sets))
      end

  fun adjustDelPiNDU (lval, pi, n, d, u) =
      let val set = getPtrSet (lval, pi)
          val rem = deleteSetPi (set, pi)

          val newPi = adjustDelSets (lval, rem)
          val n1 = adjustDelSet (lval, n)
          val d1 = adjustDelSet (lval, d)
          val u1 = adjustDelSets (lval, u)
          val pi1 = addSetPi (set, newPi)
          val _ = debugPrint (String.concat ["try to delete : ", sayPointer lval, "\n"])
          val _ = debugPrint "the \\Pi set before delete is :\n"
          val _ = printPiND (pi, n, d, u)
          val _ = debugPrint "the \\Pi set after delete is :\n"
          val _ = printPiND (pi1, n, d, u)
      in  (pi1, n1, d1, u1)
      end

  fun shrinkPiOld pi =
      let val n = PiSet.numItems pi
          fun del (lval, sets) =
              case sets
               of [] => []
                | x :: xs =>
                  if isSingletonN x
                  then if V.isPrefix (lval, List.hd (NDSet.listItems x))
                       then del (lval, xs)
                       else x :: (del (lval, xs))
                  else x :: (del (lval, xs))
          fun shrink sets =
              case sets
               of [] => []
                | x :: xs =>
                  if isSingletonN x
                  then x :: (del (List.hd (NDSet.listItems x), xs))
                  else x :: (shrink xs)
      in  PiSet.addList (emptyPi, shrink (PiSet.listItems pi))
      end

  fun shrinkPi pi =
      let val n = PiSet.numItems pi
          fun delOne (lval, sets) =
              case sets
               of [] => []
                | x :: xs =>
                  if isSingletonN x
                  then if V.isPrefix (lval, List.hd (NDSet.listItems x))
                       then delOne (lval, xs)
                       else x :: (delOne (lval, xs))
                  else x :: (delOne (lval, xs))
          fun del (lvals, sets) =
              case lvals
               of [] => []
                | x :: xs =>
                  del (xs, delOne (x, sets))
          fun shrink sets =
              case sets
               of [] => []
                | x :: xs =>
                  x :: (shrink (del (NDSet.listItems x, xs)))
      in  PiSet.addList (emptyPi, shrink (PiSet.listItems pi))
      end

  fun shrinkPi2 pi =
      let fun shrink sets =
              case sets
               of [] => []
                | x :: xs =>
                  if isSingletonN x
                  then let val lval = List.hd (NDSet.listItems x)
                       in  (addN (V.struct22id lval, emptyN)) :: (shrink xs)
                       end
                  else x :: (shrink xs)
      in  PiSet.addList (emptyPi, shrink (PiSet.listItems pi))
      end

  val iniPtrArg = ref (V.Var "@@@@")

  fun ckLval (lval, pi) =
      case lval
       of I.Var(id, pos) => ()
        | I.Ptr(_, lval1, pos) =>
          let val new_lval1 = S.tr_l lval1
          in  if isPtrInPi (new_lval1, pi)
              then ()
              else error pos ("pointer "^(sayPointer new_lval1)^" not in \\Pi set\n")
          end
        | I.Sharp _ => ()
        | I.Inarray (lval, exp, sz, pos) => (ckLval (lval, pi); ckExp (exp, pi))
        | I.Instruct(lval, id, pos) => ckLval (lval, pi)
        | _ => (debugPrint "not in ck-lval\n")

  and ckExp (exp, pi) =
      case exp
       of I.Expvoid => ()
        | I.IntNum(i) => ()
        | I.True => ()
        | I.False => ()
        | I.Null => ()
        | I.Lval(lval) => ckLval (lval, pi)
        | I.Le.BinopExp(e1, bop, e2, pos) => (ckExp (e1, pi); ckExp (e2, pi))
        | _ => (debugPrint "not impl in ck-exp\n")

  fun ckExps (es, pi) = List.app (fn e => ckExp (e, pi)) es

  fun ckAsnExp (lval1, exp, ty, pi, n, d, u, pos) : settype =
      let val _ = debugPrint "check exp in assign statement starting\n"
          val _ = ckExp (exp, pi)
          val _ = debugPrint "check exp in assign statement finished\n"
          val _ = debugPrint "check lval in assign statement starting\n"
          val _ = ckLval (lval1, pi)
          val _ = debugPrint "check lval in assign statement finished\n"
      in  case ty
           of T.Pointt _ =>
              (debugPrint "the type of this assignment is pointer type: true\n";
               case exp
                of I.Lval lval2 =>
                   let val (newLval1, newLval2) = (S.tr_l lval1, S.tr_l lval2)
                       val _ = debugPrint ("the lval being assigned is: "^(sayPointer newLval1)^"\n")
                       val _ = debugPrint "the pointer set before lval assign is:\n"
                       val _ = printPiND (pi, n, d, u)
                   in  (case (getPtrSort (newLval1, pi, n, d, u), getPtrSort (newLval2, pi, n, d, u))
                        of (Pi, Pi) =>
                           (debugPrint "(Pi, Pi)\n"
                           ; if eqN (getPtrSet (newLval1, pi), getPtrSet (newLval2, pi))
                           then (debugPrint "apply pointer logic rule: 1-(1)\n"
                               ; (pi, n, d, u))
                           else if isPtrInSingletonPi (newLval1, pi)
                                then (debugPrint "apply pointer logic rule: 1-(2)\n"
                                    ; error pos "memory leak, try to assign a singleton pointer\n"
                                    ; (pi, n, d, u))
                                else let val set2 = getPtrSet (newLval2, pi)
                                         val pi1 = deletePtrPi (newLval1, pi)
                                         val pi2 = deleteSetPi (set2, pi1)
                                         val se = addN (newLval1, set2)
                                     in  debugPrint "apply pointer logic rule: 1-(2)\n"
                                       ; (PiSet.add(pi2, se), n, d, u)
                                     end)
                         | (N, Pi) =>
                           (debugPrint "(N, Pi)\n"
                           ; debugPrint "apply pointer logic rule: 1-(3)\n"
                                ; (addPtrPi (newLval1, newLval2, pi), deletePtrN (newLval1, n), d, u))
                         | (D, Pi) =>
                           (debugPrint "(D, Pi)\n"
                           ; debugPrint "apply pointer logic rule: 1-(4)\n"
                           ; (addPtrPi (newLval1, newLval2, pi), n, deletePtrD (newLval1, d), u))
                         | (U, Pi) =>
                           (debugPrint "(U, Pi)\n"
                           ; if isPtrInU (newLval1, u)
                             then (addPtrPi (newLval1, newLval2, pi), n, d, deletePtrU (newLval1, u))
                             else (addPtrPi (newLval1, newLval2, pi), n, d, u))
                         | (Pi, N) =>
                           (debugPrint "(Pi, N)\n"
                           ; if isPtrInSingletonPi (newLval1, pi)
                             then (debugPrint "apply pointer logic rule: 1-(2)\n"
                               ; error pos "memory leak, try to assign a singleton pointer\n"
                               ; (pi, n, d, u))
                             else (deletePtrPi (newLval1, pi), addN (newLval1, n), d, u))
                         | (N, N) =>
                           (debugPrint "(N, N)\n"
                           ; (pi, n, d, u))
                         | (D, N) =>
                           (debugPrint "(D, N)\n"
                           ; (pi, addN (newLval1, n), deletePtrD (newLval1, d), u))
                         | (U, N) =>
                           (debugPrint "(U, N)\n"
                           ; if isPtrInU (newLval1, u)
                             then (pi, addN (newLval1, n), d, deletePtrU (newLval1, u))
                             else (pi, addN (newLval1, n), d,  u))
                         | (_, D) =>
                           (debugPrint "(-, U)\n"
                           ; debugPrint "apply pointer logic rule (f, f): \
                                                 \other cases in assignment\n"
                                    ; error pos "should not assign dangling pinter to other pointers\n"
                                    ; (pi, n, d, u))
                         | (Pi, U) =>
                           (debugPrint "(Pi, U)\n"
                           ; if isPtrInU (newLval2, u)
                             then if isPtrInSingletonPi (newLval1, pi)
                                  then (debugPrint "apply pointer logic rule: 1-(2)\n"
                                     ; error pos "memory leak, try to assign a singleton pointer\n"
                                     ; (pi, n, d, u))
                                  else let val _ = debugPrint "to do ajust in (Pi, U)\n"
                                           val u0 = addPtrU (newLval1, newLval2, u)
                                           val (pi1, n1, d1, u1) = adjustPiNDU (newLval1, pi, n, d, u0)
                                           val pi2 = deletePtrPi (newLval1, pi1)
                                       in  (pi2, n1, d1, u1)
                                       end
                             else if isPtrInSingletonPi (newLval1, pi)
                                  then (debugPrint "apply pointer logic rule: 1-(2)\n"
                                     ; error pos "memory leak, try to assign a singleton pointer\n"
                                     ; (pi, n, d, u))
                                  else let val _ = debugPrint "to do ajust in (Pi, U) : add U first\n"
                                           val uu = addU (newLval2, u)
                                           val u0 = addPtrU (newLval1, newLval2, uu)
                                           val (pi1, n1, d1, u1) = adjustPiNDU (newLval1, pi, n, d, u0)
                                           val pi2 = deletePtrPi (newLval1, pi)
                                       in  (pi2, n1, d1, u1)
                                       end)
                         | (N, U) =>
                           (debugPrint "(N, U)\n"
                           ; if isPtrInU (newLval2, u)
                             then (pi, deletePtrN (newLval1, n), d, addPtrU (newLval1, newLval2, u))
                             else (pi, deletePtrN (newLval1, n), d, addPtrU (newLval1, newLval2, addPi(newLval2, u))))
                         | (D, U) =>
                           (debugPrint "(D, U)\n"
                           ; if isPtrInU (newLval2, u)
                             then (pi, n, deletePtrD (newLval1, d), addPtrU (newLval1, newLval2, u))
                             else (debugPrint "to do\n"; (pi, n, d, u)))
                         | (U, U) =>
                            (debugPrint "to do\n"; (pi, n, d, u)))
                   end
                 | I.Null =>
                   let val newLval1 = S.tr_l lval1
                   in  case getPtrSort (newLval1, pi, n, d, u)
                        of Pi => if isPtrInSingletonPi (newLval1, pi)
                            then (debugPrint "apply pointer logic rule: 1-(2)\n"
                                ; error pos "memory leak, try to assign a singleton pointer\n"
                                ; (pi, n, d, u))
                            else (debugPrint "apply pointer logic rule: 1-(5)\n"
                                ; (deletePtrPi (newLval1, pi), addN (newLval1, n), d, u))
                         | N =>
                          (debugPrint "apply pointer logic rule: 1-(1)\n"
                                ; (pi, n, d, u))
                         | D =>
                          (debugPrint "apply pointer logic rule: 1-(6)\n"
                                     ; (pi, addN (newLval1, n), deletePtrD (newLval1, d), u))
                         | U =>
                           (debugPrint "delete from U\n"
                          ; if isPtrInU (newLval1, u)
                            then (pi, addN (newLval1, n), d, deletePtrU (newLval1, u))
                            else (pi, addN (newLval1, n), d, u))
                   end
                 | _ => (debugPrint "not impl in assign statement\n"
                       ; (pi, n, d, u)))
            | T.Intt =>
              (debugPrint "the type of this assignment is pointer type: false\n"
             ; debugPrint "apply pointer logic rule: 2\n"
             ; (pi, n, d, u))
            | _ =>
              (debugPrint "the type of this assignment is pointer type: true\n"
             ; debugPrint "no this type in assign-exp:\n"
             ; (pi, n, d, u))
      end

  fun ckAsnAlloc (lval, bty, pi, n, d, u, pos) : settype =
      let val _ = debugPrint "trans lval starting\n"
          val newLval = S.tr_l lval
          val _ = debugPrint "trans lval finished\n"
          val (newPi, newN, newD) =
              if isPtrInN (newLval, n)
              then let val _ = debugPrint "pointer in N\n"
                       val newPi = addPi (newLval, pi)
                       val newN = deletePtrN (newLval, n)
                   in  (newPi, newN, d)
                   end
              else if (isPtrInD (newLval, d))
                   then let val _ = debugPrint "pointer in D\n"
                            val newPi = addPi (newLval, pi)
                            val newD = deletePtrD (newLval, d)
                        in  (newPi, n, newD)
                        end
                   else if isPtrInPi (newLval, pi)
                        then let val _ = debugPrint "pointer in \\Pi set\n"
                             in  if isPtrInSingletonPi (newLval, pi)
                                 then (error pos "memory leak in assign-alloc statement\n"; (pi, n, d))
                                 else (debugPrint "not in singleton \\Pi\n"
                                    ; (addPi (newLval, deletePtrPi (newLval, pi)), n, d))
                             end
                        else (debugPrint ("where is the pointer: "^(sayPointer newLval)^"?\n")
                            ; (addPi (newLval, pi), n, d))
          fun make ty =
              case ty
               of T.Structt (strTyList, _) =>
                  let val _ = debugPrint "make function starting\n"
                      val newNewD = List.foldl (fn ((str, ty), set) =>
                                                   case ty
                                                    of T.Pointt _ => addD (V.Var (Id.toString str), set)
                                                     | _ => set)
                                               newD
                                               strTyList
                  in  (newPi, newN, newNewD, u)
                  end
                | _ => (debugPrint "the type is not a struct type in alloc\n"
                      ; (newPi, newN, newD, u))
          fun make1 (ty, (newPi, newN, newD)) =
              case ty
               of T.Ns => (newPi, newN, newD)
                | T.Voidt => (newPi, newN, newD)
                | T.Intt => (newPi, newN, newD)
                | T.Boolt => (newPi, newN, newD)
                | T.Structt (strTyList, _) =>
                  let fun doList (l, pi, n, d) =
                          case l
                           of [] => (pi, n, d)
                            | (str, ty) :: xs =>
                              case ty
                               of T.Ns => doList (xs, pi, n, d)
                                | T.Voidt => doList (xs, pi, n, d)
                                | T.Intt => doList (xs, pi, n, d)
                                | T.Boolt => doList (xs, pi, n, d)
                                | T.Structt (strTyList1, _) =>
                                  let val (resPi, resN, resD) = doList (strTyList1, pi, n, d)
                                  in  doList (xs, resPi, resN, resD)
                                  end
                                | T.Pointt ty =>
                                  let val (resPi, resN, resD) = make1 (ty, (pi, n, d))
                                      val newD = addD (V.Var (Id.toString str), resD)
                                  in  doList (xs, resPi, resN, newD)
                                  end
                                | _ => (debugPrint "not impl\n"; (pi, n, d))
                  in  doList (strTyList, newPi, newN, newD)
                  end
                | T.Arrayt (size, btype) => make1 (btype, (newPi, newN, newD))
                | T.Pointt ty => make1 (ty, (newPi, newN, newD))
                | _ => (debugPrint "compiler bug\n"; (newPi, newN, newD))
      in  (debugPrint "execute in-body starting\n"
         ; (make bty) before
          debugPrint "leave asn-alloc fun\n")
      end

  fun ckFree (e, pi, n, d, u, pos) =
      case e
       of I.Lval lval =>
          let val _ = debugPrint "the pointer sets before free are :\n"
              val _ = printPiND (pi, n, d, u)
              val newLval = S.tr_l lval
          in  case getPtrSort (newLval, pi, n, d, u)
               of Pi =>
                  if isPtrInSingletonPi (newLval, pi)
                  then let val (pi1, n1, d1, u1) = adjustDelPiNDU (newLval, pi, n, d, u)
                           val pi2 = deletePtrPi (newLval, pi1)
                           val d2 = addD (newLval, d1)
                       in  (pi2, n1, d2, u1)
                       end
                  else let val set = getPtrSet (newLval, pi)
                           val (pi1, n1, d1, u1) = adjustDelPiNDU (newLval, pi, n, d, u)
                           val _ = debugPrint "the set of the being freed value is:\n"
                           val _ = printSet set
                           val _ = debugPrint "\nthe pointer sets are :\n"
                           val _ = printPiND (pi, n, d, u)
                           val pi2 = deleteSetPi (set, pi)
                       in  debugPrint "apply poniter logic rule: 6\n"
                         ; debugPrint "\nto here: free: case 3\n"
                         ; (pi2, n1, NDSet.union (set, d1), u1)
                       end
                | N =>
                  (debugPrint "apply pointer logic rule: 6\n"
                 ; error pos "null pointer could not be freed\n"
                 ; (pi, n, d, u))
                | D =>
                  (debugPrint "apply pointer logic rule: 6\n"
                 ; error pos "dangling pointer could not be freed\n"
                 ; (pi, n, d, u))
                | U =>
                  (debugPrint "apply pointer logic rule: 6\n"
                 ; error pos "unknown pointer could not be freed\n"
                 ; (pi, n, d, u))
          end
        | I.Null =>
          (debugPrint "apply pointer logic rule: 6\n"
         ; error pos "null pointer can not be freed\n"
         ; (pi, n, d, u))
        | _ => (debugPrint "not impl in ck-free\n"; (pi, n, d, u))

  fun ckCallStm (es, pi, n, d, u) =
      let fun ck e = ckExp (e, pi)
      in  (List.app ck es; (pi, n, d, u))
      end

  fun ckRet (e, pi, n, d, u, pos) =
      let val _ = debugPrint "checking exp in return statement starting\n"
          val _ = ckExp (e, pi)
          val _ = debugPrint "checking exp in return finished\n"
      in  case e
           of I.Lval lval =>
              let val _ = debugPrint "the pointer set just before return is:\n"
                  val _ = printPiND (pi, n, d, u)
                  val newLval = S.tr_l lval
                  val newSet = getPtrSet (newLval, pi)
                  val newElm = newSet
                  val _ = debugPrint "the element to be deleted in return is:\n"
                  val _ = printN newElm
                  val newPi = deleteSetPi (newElm, pi)
                  val _ = debugPrint "the new \\Pi set after delete the return value is:\n"
                  val _ = printPiND (newPi, n, d, u)
                  fun get () =
                      let val set = getPtrSet (!iniPtrArg, newPi)
                          val pi2 = deleteSetPi (set, newPi)
                      in  pi2
                      end
              in  if eqPi(newPi, !iniPi)
                  then (newPi, n, d, u)
                  else if (!iniPtrArg) = V.Var "@@@@"
                       then (error pos "memory leak when return: some pointers have not been freed\n"
                           ; (pi, n, d, u))
                       else if eqPi (get (), !iniPi)
                            then (get (), n, d, u)
                            else (error pos "memory leak when return: some pointers have not been freed\n"
                                ; (pi, n, d, u))
              end
            | I.Expvoid =>
              let val _ = debugPrint "the \\Pi set before return is:\n"
                  val _ = printPiND (pi, n, d, u)
                  val _ = debugPrint "the initial \\Pi set before return\n"
                  val _ = printPiND (!iniPi, n, d, u)
              in  if eqPi(pi, !iniPi)
                  then (debugPrint "true branch in checking return\n"; (pi, n, d, u))
                  else (debugPrint "false branch in checking return\n";
                        error pos "memory leak when return: some pointers have not been freed\n";
                        (pi, n, d, u))
              end
            | I.IntNum _ =>
              let val _ = debugPrint "the \\Pi set before return is:\n"
                  val _ = printPiND (pi, n, d, u)
                  val _ = debugPrint "initial \\Pi set before return is:\n"
                  val _ = printPi (!iniPi)
              in  if eqPi(pi, !iniPi)
                  then (debugPrint "true branch in checking return\n"; (pi, n, d, u))
                  else (debugPrint "false branch in checking return\n";
                        error pos "memory leak when return: some pointers have not been freed\n";
                        (pi, n, d, u))
              end
            | _ => (pi, n, d, u)
      end

  fun ckAsnCall (lval, ty, es, pi, n, d, u, pos) =
      let val _ = debugPrint "check all expressions arguments in assign-call starting\n"
          val _ = ckExps (es, pi)
          val _ = debugPrint "check all expressions arguments in assign-call finished\n"
          val _ = debugPrint "check the lval in assign-call statement starting\n"
          val _ = ckLval (lval, pi)
          val _ = debugPrint "check the lval in assign-call statement finished\n"
      in  case ty
           of T.Pointt _ =>
              let val new_lval = S.tr_l lval
              in  if isPtrInSingletonPi (new_lval, pi)
                  then (error pos "memory leak in assign-call statement"; (pi, n, d, u))
                  else (pi, n, d, u)
              end
            | T.Intt => (pi, n, d, u)
            | _ => (debugPrint "not impl in assign-call statement\n"; (pi, n, d, u))
      end

  fun ckWhileStm (s, inv, cond, pi, n, d, u) =
      let val _ = ()
      in  ckStm (s, pi, n, d, u)
      end

  and ckStmIf (e, s1, s2, pi, n, d, u, pos) =
      let val _ = debugPrint "check exp in if statement starting\n"
          val _ = ckExp (e, pi)
          val _ = debugPrint "check exp in if statement finished\n"
          fun g (e, pi, n, d, u) =
              case e
               of I.Le.BinopExp (I.Lval lval, I.Equ, I.Null, pos2) =>
                  let val newLval = S.tr_l lval
                  in  case getPtrSort (S.tr_l lval, pi, n, d, u)
                       of Pi => (debugPrint "to do\n"; (pi, pi, n, n, u, newLval, 1))
                        | N => (debugPrint "to do\n"; (pi, pi, n, n, u, newLval, 1))
                        | D => (debugPrint "to do\n"; (pi, pi, n, n, u, newLval, 1))
                        | U =>
                          if isPtrInU (newLval, u)
                          then let val set = getPtrSet (newLval, u)
                               in  (pi, addSetPi (set, pi), addSetN (set, n), n,
                                    deleteSetU (set, u), newLval, 2)
                               end
                          else (pi, addPi (newLval, pi), addN (newLval, n), n, u, newLval, 2)
                  end
                | I.Le.BinopExp(I.Null, I.Equ, I.Lval(lval), pos2) =>
                  g (I.Le.BinopExp(I.Lval(lval), I.Equ,  I.Null, pos2), pi, n, d, u)
                | I.Le.BinopExp(I.Lval lval, I.NEqu, I.Null, pos2) =>
                  let val newLval = S.tr_l lval
                  in  case getPtrSort (S.tr_l lval, pi, n, d, u)
                       of Pi => raise Fail ""
                        | N => raise Fail ""
                        | D => raise Fail ""
                        | U =>
                          if isPtrInU (newLval, u)
                          then let val set = getPtrSet (newLval, u)
                               in  (addSetPi (set, pi), pi, n, addSetN (set, n),
                                    deleteSetU (set, u), newLval, 1)
                               end
                          else (addPi (newLval, pi), pi, n, addN (newLval, n), u, newLval, 1)
                  end
                | I.Le.BinopExp(I.Null, I.NEqu, I.Lval(lval), pos2) =>
                  g (I.Le.BinopExp(I.Lval(lval), I.NEqu,  I.Null, pos2), pi, n, d, u)
                | _ =>
                  (debugPrint "not impl in if test\n"
                 ; (pi, pi, n, n, u, V.Var("foo"), 1))
      in  let val (pi1, pi2, n1, n2, u1, pointer, which) = g (e, pi, n, d, u)
              val _ = debugPrint "check true branch starting\n"
              val (newPi1Pi1, newN1, newD1, newU1) = ckStm (s1, pi1, n1, d, u1)
              val _ = debugPrint "check true branch finished\n"
              val _ = debugPrint "the \\Pi set before exit true branch is:\n"
              val _ = printPiND (newPi1Pi1, newN1, newD1, newU1)
              val _ = debugPrint "check false branch starting\n"
              val (newPi2Pi2, newN2, newD2, newU2) = ckStm (s2, pi2, n2, d, u1)
              val _ = debugPrint "check false branch finished\n"
              val _ = debugPrint "the \\Pi set before exit false branch is:\n"
              val _ = printPiND (newPi2Pi2, newN2, newD2, newU2)
              val _ = (debugPrint "restore the origrinal \\Pi and N sets\n")
              val (oriPi1, oriPi2, oriN1, oriN2) =
                  case which
                   of 1 => (debugPrint (String.concat ["delete pointer: ",
                                                       (sayPointer pointer),
                                                       " from true branch starting\n"])
                          ; (if isPtrInPi (pointer, newPi1Pi1) andalso isPtrInN (pointer, newN2)
                            then (deletePtrSetPi (pointer, newPi1Pi1), newPi2Pi2, newN1,
                                  deletePtrN (pointer, newN2))
                            else (debugPrint "the pointer must have been deleted from \\Pi or N set\n";
                                  (newPi1Pi1, newPi2Pi2, newN1, newN2))) before
                           debugPrint "delete element from true branch finished\n")
                    | 2 => (debugPrint (String.concat ["delete pointer: ",
                                                       (sayPointer pointer),
                                                       " from false branch starting\n"])
                          ; if isPtrInPi (pointer, newPi2Pi2) andalso isPtrInN (pointer, newN1)
                            then (newPi1Pi1, deletePtrSetPi (pointer, newPi2Pi2),
                                  deletePtrN (pointer, newN1), newN2)
                            else (debugPrint "the pointer must have been deleted from \\Pi or N set\n";
                                  (newPi1Pi1, newPi2Pi2, newN1, newN2)))
                    | _ => raise Fail "compiler bug\n"
              val _ = debugPrint "the \\Pi and N sets just after true branch is:\n"
              val _ = printPiND (oriPi1, n, d, u)
              val _ = printN oriN1
              val _ = debugPrint "the \\Pi and N sets just after false branch is:\n"
              val _ = printPiND (oriPi2, n, d, u)
              val _ = printN oriN2
          in  if existsLongLvalPi oriPi1 orelse existsLongLvalPi oriPi2
              then (oriPi1, oriN1, newD1, u)
              else if eqPi (oriPi1, oriPi2)
                   then if eqD (newD1, newD2)
                        then (oriPi1, oriN1, newD1, u)
                        else (error pos "different D sets in two if branches\n"
                            ; (oriPi1, oriN1, newD1, u))
                   else (error pos "pointer error in if statement\n"; (oriPi1, oriN1, newD1, u))

          end
      end

  and getPiNDOne e =
      let val (pi, n, d, u) = (ref emptyPi, ref emptyN, ref emptyD, ref emptyU)
          fun get e =
              case e
               of I.Pi (lvalss, pos) => pi := (toSetSet lvalss)
                | I.N (lvals, pos) => n := (toSet lvals)
                | I.D _ => raise Fail "not impl\n"
                | I.Le.BinopExp (e1, bop, e2, pos) => (get e1; get e2)
                | I.Forall (id, ty, e1, pos) => get e1
                | I.Exists (id, ty, e1, pos) => get e1
                | _ => ()
      in  get e
        ; (!pi, !n, !d, !u)
      end

  and inv2list inv =
      case inv
       of I.Le.BinopExp (e1, I.Bor, e2, pos) => (inv2list e1) @ (inv2list e2)
        | x => [x]

  and getFromInv inv =
      List.map getPiNDOne (inv2list inv)

  and ckInvImply (pi, n, d, u, pinduList, cond, pos) =
      let val _ = debugPrint "the pointer set before imply are:\n"
          val _ = printPiND (pi, n, d, u)
      in  case cond
       of I.Le.BinopExp (I.Le.Lval lval, B.Ne, I.Null, pos) =>
          let val newLval = S.tr_l lval
              fun ck pinduList =
                  case pinduList
                   of [] => (error pos "invalid while invariant in imply\n"
                           ; (emptyPi, emptyN, emptyD, emptyU))
                    | (pix, nx, dx, ux) :: xs =>
                      (case getPtrSort (newLval, pi, n, d, u)
                        of Pi => if implyPi (pi, pix)
                                 then (pix, nx, dx, ux)
                                 else ck xs
                         | U =>
                           let val set = getPtrSet (newLval, u)
                           in  if implyPi (addSetPi (set, pi), pix)
                               then (pix, nx, dx, ux)
                               else ck xs
                           end
                         | _ => ck xs)
          in  ck pinduList
          end
        | I.Le.BinopExp (I.Null, B.Ne, I.Lval lval, pos) =>
          let val newLval = S.tr_l lval
              fun ck pinduList =
                  case pinduList
                   of [] => (error pos "invalid while invariant in imply\n"
                           ; (emptyPi, emptyN, emptyD, emptyU))
                    | (pix, nx, dx, ux) :: xs =>
                      (case getPtrSort (newLval, pix, nx, dx, ux)
                        of Pi => if implyPi (pi, pix)
                                 then (pix, nx, dx, ux)
                                 else ck xs
                         | U =>
                           let val set = getPtrSet (newLval, ux)
                           in  if implyPi (pi, ux)
                               then (pix, nx, dx, ux)
                               else ck xs
                           end
                         | _ => ck xs)
          in  ck pinduList
          end
        | _ => (debugPrint "always integer comparasion?\n"
        ; let val _ = ()
              fun ck pinduList =
                  case pinduList
                   of [] => (error pos "invalid while invariant in imply\n"
                           ; (emptyPi, emptyN, emptyD, emptyU))
                    | (pix, nx, dx, ux) :: xs =>
                      if implyPi (pi, pix)
                      then (pix, nx, dx, ux)
                      else ck xs
          in  ck pinduList
          end)
      end

  and getPostInv (pi, n, d, u, pinduList, cond, pos) =
      case cond
       of I.Le.BinopExp (I.Le.Lval lval, B.Ne, I.Null, pos) =>
          let val newLval = S.tr_l lval
              fun ck pinduList =
                  case pinduList
                   of [] => (error pos "invalid while invariant get\n"
                           ; (emptyPi, emptyN, emptyD, emptyU))
                    | (pix, nx, dx, ux) :: xs =>
                      if isPtrInN (newLval, nx)
                      then (pix, nx, dx, ux)
                      else ck xs
          in  ck pinduList
          end
        | I.Le.BinopExp (I.Null, B.Ne, I.Lval lval, pos) =>
          let val newLval = S.tr_l lval
              fun ck pinduList =
                  case pinduList
                   of [] => (error pos "invalid while invariant in get\n"
                           ; (emptyPi, emptyN, emptyD, emptyU))
                    | (pix, nx, dx, ux) :: xs =>
                      if isPtrInN (newLval, nx)
                      then (pix, nx, dx, ux)
                      else ck xs
          in  ck pinduList
          end
        | _ =>
         (debugPrint "always integer comparasion?\n"
        ; let val _ = ()
              fun ck pinduList =
                  case pinduList
                   of [] => (error pos "invalid while invariant in get\n"
                           ; (emptyPi, emptyN, emptyD, emptyU))
                    | (pix, nx, dx, ux) :: xs =>
                      if eqPi (pi, pix)
                      then (pix, nx, dx, ux)
                      else ck xs
          in  ck pinduList
          end)

  and ckPostInvImply2 (pi, n, d, u, pinduList, pos) =
      let val _ = debugPrint "the \\Pi N D before shrink2 is:\n"
          val _ = printPiND (pi, n, d, u)
          val newPi = shrinkPi2 pi
          val _ = debugPrint "the \\Pi N D after shrink2 is:\n"
          val _ = printPiND (newPi, n, d, u)
          fun ck l =
              case l
               of [] => error pos "invalid while invariant in post-imply\n"
                | (pix, nx, dx, ux) :: xs =>
                  if postImplyPi (newPi, pix)
                  then ()
                  else ck xs
      in  ck pinduList
      end

  and ckPostInvImply (pi, n, d, u, cond, pinduList, pos) =
      let val _ = debugPrint "the \\Pi N D before shrink is:\n"
          val _ = printPiND (pi, n, d, u)
          val newPi = shrinkPi pi
          val _ = debugPrint "the \\Pi N D after shrink is:\n"
          val _ = printPiND (newPi, n, d, u)
          fun ck l =
              case l
               of [] => ckPostInvImply2 (newPi, n, d, u, pinduList, pos)
                | (pix, nx, dx, ux) :: xs =>
                  if postImplyPi (newPi, pix) andalso postImplyN (n, nx)
                  then ()
                  else ck xs
      in  ck pinduList
      end



  and ckStm (s, pi, n, d, u) : settype =
      case s
       of I.Skip =>
          (debugPrint "no other statement exists, all finished\n"
         ; (pi, n, d, u))
        | I.AsnExp(lval, exp, ty, pos) =>
          let val _ = debugPrint (String.concat ["check assign exp statement starting: ",
                                                 sayPointer (S.tr_l lval),
                                                 "=...\n"])
              val _ = debugPrint "the initial \\Pi, N, D and U are: \n\n"
              val _ = printPiND (pi, n, d, u)
              val (npi, nn, nd, nu) = ckAsnExp (lval, exp, ty, pi, n, d, u, pos)
          in  debugPrint "the pointer set after assign is:\n"
             ; printPiND (npi, nn, nd, nu)
             ; debugPrint "check assign exp statement finished\n"
             ; (npi, nn, nd, nu)
          end
        | I.AsnAlloc (lval, ty, bty, pos) =>
          let val _ = debugPrint (String.concat ["check assign alloc statement starting: ",
                                                 sayPointer (S.tr_l lval),
                                                 "=...\n"])
          in  ckAsnAlloc (lval, bty, pi, n, d, u, pos) before
              debugPrint "check assign alloc statement finished\n"
          end
        | I.AsnCall (lval, id, es, ty, pos) => ckAsnCall (lval, ty, es, pi, n, d, u, pos)
        | I.Seq(s1, s2, pos) =>
          let val (newPi, newN, newD, newU) = ckStm (s1, pi, n, d, u)
          in  ckStm (s2, newPi, newN, newD, newU)
          end
        | I.If (e, s1, s2, pos) =>
          let val _ = debugPrint ("check if statement starting\n")
          in  ckStmIf (e, s1, s2, pi, n, d, u, pos) before
              debugPrint ("check if statement finished\n")
          end
        | I.While (inv, cond, s, pos) =>
          let val newPiNDlist = getFromInv inv
              val _ = debugPrint "the \\Pi set in invariant is:\n"
              val _ = List.app printPiND newPiNDlist
              val _ = debugPrint "check while invariant imply starting\n"
              val (bodyPi, bodyN, bodyD, bodyU) =
                      if List.null newPiNDlist
                      then (emptyPi, emptyN, emptyD, emptyU)
                      else ckInvImply (pi, n, d, u, newPiNDlist, cond, pos)
              val _ = debugPrint "check while invariant imply finished\n"
              val _ = debugPrint "get post-inv starting\n"
              val (postPi, postN, postD, postU) =
                      if List.null newPiNDlist
                      then (emptyPi, emptyN, emptyD, emptyU)
                      else getPostInv (pi, n, d, u, newPiNDlist, cond, pos)
              val _ = debugPrint "get post-inv finished\n"
              val _ = debugPrint "the post-inv are:\n"
              val _ = printPiND (postPi, postN, postD, postU)
              val _ = debugPrint "check while-body statements starting\n"
              val (wPi, wN, wD, wU) = ckWhileStm (s, inv, cond, bodyPi, bodyN, bodyD, bodyU)
              val _ = debugPrint "check while-body statements finished\n"
              val _ = debugPrint "check while-body invariant post-imply starting\n"
              val _ = if List.null newPiNDlist
                      then ()
                      else ckPostInvImply (wPi, wN, wD, wU, cond, newPiNDlist, pos)
              val _ = debugPrint "check while-body invariant post-imply finished\n"
          in  (postPi, postN, postD, postU)
          end
        | I.Return (exp, pos) =>
          let val _ = debugPrint "check return statement starting\n"
          in  ckRet (exp, pi, n, d, u, pos) before
              debugPrint "check return statement finished\n"
          end
        | I.Call (id, es, pos) =>
          let val _ = debugPrint "check return statement starting\n"
          in  ckCallStm (es, pi, n, d, u) before
              debugPrint "check call statement finished\n"
          end
        | I.Free (e, pos) =>
          let val _ = debugPrint "check free statement starting\n"
              val (npi, nn, nd, nu) = ckFree (e, pi, n, d, u, pos)
          in  debugPrint "the pointer set after free is:\n"
             ; printPiND (npi, nn, nd, nu)
             ; debugPrint "check free statement finished\n"
             ; (npi, nn, nd, nu)
          end
        | I.Prop(e, pos) => (debugPrint "not impl\n"; (pi, n, d, u))

  fun getPiND (set, l) =
      case l
       of [] => set
        | (id, ty) :: xs =>
          case ty
           of I.Pointer _ => getPiND ((addD (V.Var (Id.toString id), set)), xs)
            | _ => getPiND (set, xs)

  fun getPtrArg args =
      case args
       of [] => V.Var "@@@@"
        | (id, ty) :: xs =>
          case ty
           of I.Pointer _ => V.Var (Id.toString id)
            | _ => getPtrArg xs

  fun ckDec ir =
      case ir
       of I.ExdecSkip => ()
        | I.ExdecSeq (d1, d2, pos) => (ckDec d1; ckDec d2)
        | I.ExdecStruct (_, _, _) => ()
        | I.ExdecVar (_, _) => ()
        | I.ExdecFunc (_, _, args, locals, stm, pre, post, pos) =>
          let val _ = iniPtrArg := getPtrArg args
              fun spilt exp =
                  case exp
                   of I.Pi(lvalss, pos) => toSetSet lvalss
                    | I.Le.BinopExp(e1, bop, e2, pos) => spilt e1
                    | _ => emptyPi
              fun spiltU exp =
                  case exp
                   of I.Let (e1, e2, e3, pos) =>
                      (case e3
                        of I.LList ((I.Lval lval), _) => addPi (S.tr_l lval, emptyU)
                         | I.Tree ((I.Lval lval), _) => addPi (S.tr_l lval, emptyU)
                         | _ => emptyU)
                    | _ => emptyU
              val pi = spilt pre
              val _ = (iniPi := pi)
              val u = spiltU pre
              val _ = debugPrint "the initial \\Pi N D U are:\n"
              val _ = printPiND (pi, emptyN, emptyD, u)
              val newD = getPiND (emptyD, locals)
              val _ = debugPrint "the got \\Pi N D U are:\n"
              val _ = printPiND (pi, emptyN, newD, u)
          in  ckStm (stm, pi, emptyN, newD, u)
             ; ()
          end

  fun top ir =
      let val _ = resetIniPi ()
      in  ckDec ir
      end
end
